\begin{tabbing}
es{-}responsive(${\it es}$;$l_{1}$;${\it tg}_{1}$;$l_{2}$;${\it tg}_{2}$)
\\[0ex]$\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$\=alle{-}rcv(${\it es}$;$l_{1}$;${\it tg}_{1}$;$e$.existse{-}rcv(${\it es}$;$l_{2}$;${\it tg}_{2}$;${\it e'}$.es{-}le(${\it es}$;$e$;es{-}sender(${\it es}$; ${\it e'}$))\+
\\[0ex]\& alle{-}rcv(${\it es}$;$l_{1}$;${\it tg}_{1}$;$e_{2}$.es{-}locl(${\it es}$; $e$; $e_{2}$) $\Rightarrow$ es{-}locl(${\it es}$; es{-}sender(${\it es}$; ${\it e'}$); $e_{2}$))
\\[0ex]\& alle{-}rcv(${\it es}$;$l_{2}$;${\it tg}_{2}$;${\it e''}$.\=es{-}sender(${\it es}$; ${\it e''}$) $=$ es{-}sender(${\it es}$; ${\it e'}$) $\in$ es{-}E(${\it es}$)\+
\\[0ex]$\Rightarrow$ ${\it e''}$ $=$ ${\it e'}$ $\in$ es{-}E(${\it es}$))))
\-\\[0ex]\& \=alle{-}rcv(${\it es}$;$l_{2}$;${\it tg}_{2}$;${\it e'}$.existse{-}rcv(${\it es}$;$l_{1}$;${\it tg}_{1}$;$e$.es{-}le(${\it es}$;$e$;es{-}sender(${\it es}$; ${\it e'}$))\+
\\[0ex]\& alle{-}rcv(${\it es}$;$l_{2}$;${\it tg}_{2}$;${\it e''}$.\=es{-}locl(${\it es}$; es{-}sender(${\it es}$; ${\it e''}$); es{-}sender(${\it es}$; ${\it e'}$))\+
\\[0ex]$\Rightarrow$ es{-}locl(${\it es}$; es{-}sender(${\it es}$; ${\it e''}$); $e$))))
\-\-\-
\end{tabbing}